abstract sig Person {
  parents: lone Couple,
}

sig Couple {
  father: one Male,
  mother: one Female,
  children: set (ChildMale + ChildFemale),
}

abstract sig Male extends Person { }
abstract sig Female extends Person { }

sig ChildMale extends Male { } { one parents }
sig ChildFemale extends Female { } { one parents }

one sig Adam extends Male { } { no parents }
one sig Eve extends Female { } { no parents }
one sig RootCouple extends Couple { }

fact oneRootCouple { 
  one r: RootCouple | 
    r.father = Adam and 
    r.mother = Eve
}

// You cannot be your own parent.
fact validParents { 
  no p: Person | 
    p.^(parents.father) = p or
    p.^(parents.mother) = p
}

// Connect the children with their parents.
fact connectParents {
  all c: Couple, ch: c.children |
    ch.parents = c
}
fact connectChildren {
  all p: (ChildMale + ChildFemale) |
    p in p.parents.children
}

// TODO Indicate that we have one connected tree where all children 
// have directly or indirectly been made by Adam and Eve.

// Acyclic relationship
fact acyclic {
  no p: Person |
    p in (p.^(parents.father) + p.^(parents.mother))
}

// Children may never appear above in the tree of their parents
fact {
  no c: Couple, ch: c.children |
    ch in c.father.^(parents.father) + c.father.^(parents.mother) or
    ch in c.mother.^(parents.father) + c.mother.^(parents.father)
}

// Couples have to be unique
fact uniqueCouple { 
  no c: Couple | 
    c.father in (Couple - c).father or
		c.mother in (Couple - c).mother
}

// Predicates
pred grandfather[p: Person, pGrandfather: Person] {
  p.parents.father.parents.father = pGrandfather or
  p.parents.mother.parents.father = pGrandfather
}

pred grandmother[p: Person, pGrandmother: Person] {
  p.parents.father.parents.mother = pGrandmother or
  p.parents.mother.parents.mother = pGrandmother
}

pred sibling[p: Person, pSibling: Person] {
  p.parents = pSibling.parents
}

pred brother[p: Person, pBrother: Person] {
  sibling[p, pBrother] and pBrother in Male
}

pred sister[p: Person, pSister: Person] {
  sibling[p, pSister] and pSister in Female
}

pred child[p: Person, pChild: Person] {
   pChild.parents.father = p or pChild.parents.mother = p
}

pred grandchild[p: Person, pGrandchild: Person] {
   grandmother[pGrandchild, p] or grandfather[pGrandchild, p]
}

pred uncle[p: Person, pUncle: Person] {
  brother[p.parents.father, pUncle] or brother[p.parents.mother, pUncle]
}

pred aunt[p: Person, pAunt: Person] {
  sister[p.parents.father, pAunt] or sister[p.parents.mother, pAunt]
}

pred cousin[p: Person, pCousin: Person] {
  uncle[pCousin, p] or aunt[pCousin, p]
}

pred nephew[p: Person, pNephew: Person] {
  cousin[p, pNephew] and pNephew in Male
}

pred niece[p: Person, pNiece: Person] {
  cousin[p, pNiece] and pNiece in Female
}

// The royal family scenario for testing
one sig JulianaBernhard, BeatrixClaus, MaximaWA extends Couple { }

one sig Juliana, Beatrix, Irene, Maxima, Amalia, Alexia, Ariane extends ChildFemale { }
one sig Bernhard, Claus, WA, Friso, Constantijn extends ChildMale { }

fact royalFamily {
  JulianaBernhard.mother = Juliana
  JulianaBernhard.father = Bernhard
  BeatrixClaus.mother = Beatrix
  BeatrixClaus.father = Claus
  MaximaWA.mother = Maxima
  MaximaWA.father = WA

  JulianaBernhard.children = (Irene + Beatrix)
  BeatrixClaus.children = (WA + Friso + Constantijn)
  MaximaWA.children = (Amalia + Alexia + Ariane)
}

pred assertRoyalFamily {
  grandfather[WA, Bernhard]
  grandmother[WA, Juliana]
  brother[WA, Friso]
  brother[WA, Constantijn]
  sister[Amalia, Alexia]
  sister[Amalia, Ariane]
  sister[Alexia, Ariane]
  child[WA, Amalia]
  child[Maxima, Amalia]
  grandchild[Bernhard, WA]
  not grandchild[Bernhard, Amalia]
  uncle[Amalia, Friso]
  aunt[WA, Irene]
  nephew[Irene, WA]
  not nephew[Friso, Amalia]
  niece[Friso, Amalia]
}

run assertRoyalFamily for 14 Person, 4 Couple

// Indication of time spent: 12,5 hours per team member
